home *** CD-ROM | disk | FTP | other *** search
/ Shareware Grab Bag / Shareware Grab Bag.iso / 090 / byte0487.arc / TELLO.ARC / BOYER.LSP next >
Encoding:
Text File  |  1980-01-01  |  13.0 KB  |  540 lines
  1. ; BOYER
  2.  
  3. (defvar unify-subst)
  4. (defvar temp-temp)
  5.  
  6. (DEFUN ADD-LEMMA (TERM)
  7.   (COND ((AND (NOT (ATOM TERM))
  8.           (EQ (CAR TERM)
  9.           (QUOTE EQUAL))
  10.           (NOT (ATOM (CADR TERM))))
  11.      ;; This change lets you run setup several times.
  12.      (unless (member term (get (car (cadr term)) 'lemmas) :test #'equal)
  13.        (SETF (GET (CAR (CADR TERM)) (QUOTE LEMMAS))
  14.          (CONS TERM (GET (CAR (CADR TERM)) (QUOTE LEMMAS))))))
  15.     (T
  16.      (error "Add lemma did not like term")
  17.      )))
  18.  
  19. (DEFUN ADD-LEMMA-LST (LST)
  20.        (COND ((NULL LST)
  21.           T)
  22.          (T (ADD-LEMMA (CAR LST))
  23.         (ADD-LEMMA-LST (CDR LST)))))
  24.  
  25. (DEFUN APPLY-SUBST (ALIST TERM)
  26.        (COND ((ATOM TERM)
  27.           (COND ((SETQ TEMP-TEMP (ASSOC TERM ALIST))
  28.              (CDR TEMP-TEMP))
  29.             (T TERM)))
  30.          (T (CONS (CAR TERM)
  31.               (APPLY-SUBST-LST ALIST (CDR TERM))))))
  32.  
  33. (DEFUN APPLY-SUBST-LST (ALIST LST)
  34.        (COND ((NULL LST)
  35.           NIL)
  36.          (T (CONS (APPLY-SUBST ALIST (CAR LST))
  37.               (APPLY-SUBST-LST ALIST (CDR LST))))))
  38.  
  39. (DEFUN FALSEP (X LST)
  40.        (OR (EQUAL X (QUOTE (F)))
  41.        (MEMBER X LST)))
  42.  
  43. (DEFUN ONE-WAY-UNIFY (TERM1 TERM2)
  44.        (PROGN (SETQ UNIFY-SUBST NIL)
  45.           (ONE-WAY-UNIFY1 TERM1 TERM2)))
  46.  
  47. (DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2)
  48.        (COND ((ATOM TERM2)
  49.           (COND ((SETQ TEMP-TEMP (ASSOC TERM2 UNIFY-SUBST))
  50.              (EQUAL TERM1 (CDR TEMP-TEMP)))
  51.             (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
  52.                            UNIFY-SUBST))
  53.                T)))
  54.          ((ATOM TERM1)
  55.           NIL)
  56.          ((EQ (CAR TERM1)
  57.           (CAR TERM2))
  58.           (ONE-WAY-UNIFY1-LST (CDR TERM1)
  59.                   (CDR TERM2)))
  60.          (T NIL)))
  61.  
  62. (DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2)
  63.        (COND ((NULL LST1)
  64.           T)
  65.          ((ONE-WAY-UNIFY1 (CAR LST1)
  66.                   (CAR LST2))
  67.           (ONE-WAY-UNIFY1-LST (CDR LST1)
  68.                   (CDR LST2)))
  69.          (T NIL)))
  70.  
  71. (DEFUN REWRITE (TERM)
  72.        (COND ((ATOM TERM)
  73.           TERM)
  74.          (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
  75.                        (REWRITE-ARGS (CDR TERM)))
  76.                      (GET (CAR TERM)
  77.                           (QUOTE LEMMAS))))))
  78.  
  79. (DEFUN REWRITE-ARGS (LST)
  80.        (COND ((NULL LST)
  81.           NIL)
  82.          (T (CONS (REWRITE (CAR LST))
  83.               (REWRITE-ARGS (CDR LST))))))
  84.  
  85. (DEFUN REWRITE-WITH-LEMMAS (TERM LST)
  86.        (COND ((NULL LST)
  87.           TERM)
  88.          ((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
  89.           (REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
  90.          (T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
  91.  
  92. (DEFUN SETUP ()
  93.   (ADD-LEMMA-LST
  94.     (QUOTE ((EQUAL (COMPILE FORM)
  95.            (REVERSE (CODEGEN (OPTIMIZE FORM)
  96.                      (NIL))))
  97.         (EQUAL (EQP X Y)
  98.            (EQUAL (FIX X)
  99.               (FIX Y)))
  100.         (EQUAL (GREATERP X Y)
  101.            (LESSP Y X))
  102.         (EQUAL (LESSEQP X Y)
  103.            (NOT (LESSP Y X)))
  104.         (EQUAL (GREATEREQP X Y)
  105.            (NOT (LESSP X Y)))
  106.         (EQUAL (BOOLEAN X)
  107.            (OR (EQUAL X (T))
  108.                (EQUAL X (F))))
  109.         (EQUAL (IFF X Y)
  110.            (AND (IMPLIES X Y)
  111.             (IMPLIES Y X)))
  112.         (EQUAL (EVEN1 X)
  113.            (IF (ZEROP X)
  114.                (T)
  115.                (ODD (1- X))))
  116.         (EQUAL (COUNTPS- L PRED)
  117.            (COUNTPS-LOOP L PRED (ZERO)))
  118.         (EQUAL (FACT- I)
  119.            (FACT-LOOP I 1))
  120.         (EQUAL (REVERSE- X)
  121.            (REVERSE-LOOP X (NIL)))
  122.         (EQUAL (DIVIDES X Y)
  123.            (ZEROP (remainder Y X)))
  124.         (EQUAL (ASSUME-TRUE VAR ALIST)
  125.            (CONS (CONS VAR (T))
  126.              ALIST))
  127.         (EQUAL (ASSUME-FALSE VAR ALIST)
  128.            (CONS (CONS VAR (F))
  129.              ALIST))
  130.         (EQUAL (TAUTOLOGY-CHECKER X)
  131.            (TAUTOLOGYP (NORMALIZE X)
  132.                    (NIL)))
  133.         (EQUAL (FALSIFY X)
  134.            (FALSIFY1 (NORMALIZE X)
  135.                  (NIL)))
  136.         (EQUAL (PRIME X)
  137.            (AND (NOT (ZEROP X))
  138.             (NOT (EQUAL X (ADD1 (ZERO))))
  139.             (PRIME1 X (1- X))))
  140.         (EQUAL (AND P Q)
  141.            (IF P (IF Q (T)
  142.                  (F))
  143.                (F)))
  144.         (EQUAL (OR P Q)
  145.            (IF P (T)
  146.                (IF Q (T)
  147.                (F))
  148.                (F)))
  149.         (EQUAL (NOT P)
  150.            (IF P (F)
  151.                (T)))
  152.         (EQUAL (IMPLIES P Q)
  153.            (IF P (IF Q (T)
  154.                  (F))
  155.                (T)))
  156.         (EQUAL (FIX X)
  157.            (IF (NUMBERP X)
  158.                X
  159.                (ZERO)))
  160.         (EQUAL (IF (IF A B C)
  161.                D E)
  162.            (IF A (IF B D E)
  163.                (IF C D E)))
  164.         (EQUAL (ZEROP X)
  165.            (OR (EQUAL X (ZERO))
  166.                (NOT (NUMBERP X))))
  167.         (EQUAL (PLUS (PLUS X Y)
  168.              Z)
  169.            (PLUS X (PLUS Y Z)))
  170.         (EQUAL (EQUAL (PLUS A B)
  171.               (ZERO))
  172.            (AND (ZEROP A)
  173.             (ZEROP B)))
  174.         (EQUAL (DIFFERENCE X X)
  175.            (ZERO))
  176.         (EQUAL (EQUAL (PLUS A B)
  177.               (PLUS A C))
  178.            (EQUAL (FIX B)
  179.               (FIX C)))
  180.         (EQUAL (EQUAL (ZERO)
  181.               (DIFFERENCE X Y))
  182.            (NOT (LESSP Y X)))
  183.         (EQUAL (EQUAL X (DIFFERENCE X Y))
  184.            (AND (NUMBERP X)
  185.             (OR (EQUAL X (ZERO))
  186.                 (ZEROP Y))))
  187.         (EQUAL (MEANING (PLUS-TREE (APPEND X Y))
  188.                 A)
  189.            (PLUS (MEANING (PLUS-TREE X)
  190.                   A)
  191.              (MEANING (PLUS-TREE Y)
  192.                   A)))
  193.         (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
  194.                 A)
  195.            (FIX (MEANING X A)))
  196.         (EQUAL (APPEND (APPEND X Y)
  197.                Z)
  198.            (APPEND X (APPEND Y Z)))
  199.         (EQUAL (REVERSE (APPEND A B))
  200.            (APPEND (REVERSE B)
  201.                (REVERSE A)))
  202.         (EQUAL (TIMES X (PLUS Y Z))
  203.            (PLUS (TIMES X Y)
  204.              (TIMES X Z)))
  205.         (EQUAL (TIMES (TIMES X Y)
  206.               Z)
  207.            (TIMES X (TIMES Y Z)))
  208.         (EQUAL (EQUAL (TIMES X Y)
  209.               (ZERO))
  210.            (OR (ZEROP X)
  211.                (ZEROP Y)))
  212.         (EQUAL (EXEC (APPEND X Y)
  213.              PDS ENVRN)
  214.            (EXEC Y (EXEC X PDS ENVRN)
  215.              ENVRN))
  216.         (EQUAL (MC-FLATTEN X Y)
  217.            (APPEND (FLATTEN X)
  218.                Y))
  219.         (EQUAL (MEMBER X (APPEND A B))
  220.            (OR (MEMBER X A)
  221.                (MEMBER X B)))
  222.         (EQUAL (MEMBER X (REVERSE Y))
  223.            (MEMBER X Y))
  224.         (EQUAL (LENGTH (REVERSE X))
  225.            (LENGTH X))
  226.         (EQUAL (MEMBER A (INTERSECT B C))
  227.            (AND (MEMBER A B)
  228.             (MEMBER A C)))
  229.         (EQUAL (NTH (ZERO)
  230.             I)
  231.            (ZERO))
  232.         (EQUAL (EXP I (PLUS J K))
  233.            (TIMES (EXP I J)
  234.               (EXP I K)))
  235.         (EQUAL (EXP I (TIMES J K))
  236.            (EXP (EXP I J)
  237.             K))
  238.         (EQUAL (REVERSE-LOOP X Y)
  239.            (APPEND (REVERSE X)
  240.                Y))
  241.         (EQUAL (REVERSE-LOOP X (NIL))
  242.            (REVERSE X))
  243.         (EQUAL (COUNT-LIST Z (SORT-LP X Y))
  244.            (PLUS (COUNT-LIST Z X)
  245.              (COUNT-LIST Z Y)))
  246.         (EQUAL (EQUAL (APPEND A B)
  247.               (APPEND A C))
  248.            (EQUAL B C))
  249.         (EQUAL (PLUS (REMAINDER X Y)
  250.              (TIMES Y (QUOTIENT X Y)))
  251.            (FIX X))
  252.         (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
  253.                    BASE)
  254.            (PLUS (POWER-EVAL L BASE)
  255.              I))
  256.         (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
  257.                    BASE)
  258.            (PLUS I (PLUS (POWER-EVAL X BASE)
  259.                  (POWER-EVAL Y BASE))))
  260.         (EQUAL (REMAINDER Y 1)
  261.            (ZERO))
  262.         (EQUAL (LESSP (REMAINDER X Y)
  263.               Y)
  264.            (NOT (ZEROP Y)))
  265.         (EQUAL (REMAINDER X X)
  266.            (ZERO))
  267.         (EQUAL (LESSP (QUOTIENT I J)
  268.               I)
  269.            (AND (NOT (ZEROP I))
  270.             (OR (ZEROP J)
  271.                 (NOT (EQUAL J 1)))))
  272.         (EQUAL (LESSP (REMAINDER X Y)
  273.               X)
  274.            (AND (NOT (ZEROP Y))
  275.             (NOT (ZEROP X))
  276.             (NOT (LESSP X Y))))
  277.         (EQUAL (POWER-EVAL (POWER-REP I BASE)
  278.                    BASE)
  279.            (FIX I))
  280.         (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
  281.                      (POWER-REP J BASE)
  282.                      (ZERO)
  283.                      BASE)
  284.                    BASE)
  285.            (PLUS I J))
  286.         (EQUAL (GCD X Y)
  287.            (GCD Y X))
  288.         (EQUAL (NTH (APPEND A B)
  289.             I)
  290.            (APPEND (NTH A I)
  291.                (NTH B (DIFFERENCE I (LENGTH A)))))
  292.         (EQUAL (DIFFERENCE (PLUS X Y)
  293.                    X)
  294.            (FIX Y))
  295.         (EQUAL (DIFFERENCE (PLUS Y X)
  296.                    X)
  297.            (FIX Y))
  298.         (EQUAL (DIFFERENCE (PLUS X Y)
  299.                    (PLUS X Z))
  300.            (DIFFERENCE Y Z))
  301.         (EQUAL (TIMES X (DIFFERENCE C W))
  302.            (DIFFERENCE (TIMES C X)
  303.                    (TIMES W X)))
  304.         (EQUAL (REMAINDER (TIMES X Z)
  305.                   Z)
  306.            (ZERO))
  307.         (EQUAL (DIFFERENCE (PLUS B (PLUS A C))
  308.                    A)
  309.            (PLUS B C))
  310.         (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
  311.                    Z)
  312.            (ADD1 Y))
  313.         (EQUAL (LESSP (PLUS X Y)
  314.               (PLUS X Z))
  315.            (LESSP Y Z))
  316.         (EQUAL (LESSP (TIMES X Z)
  317.               (TIMES Y Z))
  318.            (AND (NOT (ZEROP Z))
  319.             (LESSP X Y)))
  320.         (EQUAL (LESSP Y (PLUS X Y))
  321.            (NOT (ZEROP X)))
  322.         (EQUAL (GCD (TIMES X Z)
  323.             (TIMES Y Z))
  324.            (TIMES Z (GCD X Y)))
  325.         (EQUAL (VALUE (NORMALIZE X)
  326.               A)
  327.            (VALUE X A))
  328.         (EQUAL (EQUAL (FLATTEN X)
  329.               (CONS Y (NIL)))
  330.            (AND (NLISTP X)
  331.             (EQUAL X Y)))
  332.         (EQUAL (LISTP (GOPHER X))
  333.            (LISTP X))
  334.         (EQUAL (SAMEFRINGE X Y)
  335.            (EQUAL (FLATTEN X)
  336.               (FLATTEN Y)))
  337.         (EQUAL (EQUAL (GREATEST-FACTOR X Y)
  338.               (ZERO))
  339.            (AND (OR (ZEROP Y)
  340.                 (EQUAL Y 1))
  341.             (EQUAL X (ZERO))))
  342.         (EQUAL (EQUAL (GREATEST-FACTOR X Y)
  343.               1)
  344.            (EQUAL X 1))
  345.         (EQUAL (NUMBERP (GREATEST-FACTOR X Y))
  346.            (NOT (AND (OR (ZEROP Y)
  347.                  (EQUAL Y 1))
  348.                  (NOT (NUMBERP X)))))
  349.         (EQUAL (TIMES-LIST (APPEND X Y))
  350.            (TIMES (TIMES-LIST X)
  351.               (TIMES-LIST Y)))
  352.         (EQUAL (PRIME-LIST (APPEND X Y))
  353.            (AND (PRIME-LIST X)
  354.             (PRIME-LIST Y)))
  355.         (EQUAL (EQUAL Z (TIMES W Z))
  356.            (AND (NUMBERP Z)
  357.             (OR (EQUAL Z (ZERO))
  358.                 (EQUAL W 1))))
  359.         (EQUAL (GREATEREQPR X Y)
  360.            (NOT (LESSP X Y)))
  361.         (EQUAL (EQUAL X (TIMES X Y))
  362.            (OR (EQUAL X (ZERO))
  363.                (AND (NUMBERP X)
  364.                 (EQUAL Y 1))))
  365.         (EQUAL (REMAINDER (TIMES Y X)
  366.                   Y)
  367.            (ZERO))
  368.         (EQUAL (EQUAL (TIMES A B)
  369.               1)
  370.            (AND (NOT (EQUAL A (ZERO)))
  371.             (NOT (EQUAL B (ZERO)))
  372.             (NUMBERP A)
  373.             (NUMBERP B)
  374.             (EQUAL (1- A)
  375.                    (ZERO))
  376.             (EQUAL (1- B)
  377.                    (ZERO))))
  378.         (EQUAL (LESSP (LENGTH (DELETE X L))
  379.               (LENGTH L))
  380.            (MEMBER X L))
  381.         (EQUAL (SORT2 (DELETE X L))
  382.            (DELETE X (SORT2 L)))
  383.         (EQUAL (DSORT X)
  384.            (SORT2 X))
  385.         (EQUAL (LENGTH (CONS X1
  386.                  (CONS X2
  387.                        (CONS X3 (CONS X4
  388.                               (CONS X5
  389.                                 (CONS X6 X7)))))))
  390.            (PLUS 6 (LENGTH X7)))
  391.         (EQUAL (DIFFERENCE (ADD1 (ADD1 X))
  392.                    2)
  393.            (FIX X))
  394.         (EQUAL (QUOTIENT (PLUS X (PLUS X Y))
  395.                  2)
  396.            (PLUS X (QUOTIENT Y 2)))
  397.         (EQUAL (SIGMA (ZERO)
  398.               I)
  399.            (QUOTIENT (TIMES I (ADD1 I))
  400.                  2))
  401.         (EQUAL (PLUS X (ADD1 Y))
  402.            (IF (NUMBERP Y)
  403.                (ADD1 (PLUS X Y))
  404.                (ADD1 X)))
  405.         (EQUAL (EQUAL (DIFFERENCE X Y)
  406.               (DIFFERENCE Z Y))
  407.            (IF (LESSP X Y)
  408.                (NOT (LESSP Y Z))
  409.                (IF (LESSP Z Y)
  410.                (NOT (LESSP Y X))
  411.                (EQUAL (FIX X)
  412.                   (FIX Z)))))
  413.         (EQUAL (MEANING (PLUS-TREE (DELETE X Y))
  414.                 A)
  415.            (IF (MEMBER X Y)
  416.                (DIFFERENCE (MEANING (PLUS-TREE Y)
  417.                         A)
  418.                    (MEANING X A))
  419.                (MEANING (PLUS-TREE Y)
  420.                 A)))
  421.         (EQUAL (TIMES X (ADD1 Y))
  422.            (IF (NUMBERP Y)
  423.                (PLUS X (TIMES X Y))
  424.                (FIX X)))
  425.         (EQUAL (NTH (NIL)
  426.             I)
  427.            (IF (ZEROP I)
  428.                (NIL)
  429.                (ZERO)))
  430.         (EQUAL (LAST (APPEND A B))
  431.            (IF (LISTP B)
  432.                (LAST B)
  433.                (IF (LISTP A)
  434.                (CONS (CAR (LAST A))
  435.                  B)
  436.                B)))
  437.         (EQUAL (EQUAL (LESSP X Y)
  438.               Z)
  439.            (IF (LESSP X Y)
  440.                (EQUAL T Z)
  441.                (EQUAL F Z)))
  442.         (EQUAL (ASSIGNMENT X (APPEND A B))
  443.            (IF (ASSIGNEDP X A)
  444.                (ASSIGNMENT X A)
  445.                (ASSIGNMENT X B)))
  446.         (EQUAL (CAR (GOPHER X))
  447.            (IF (LISTP X)
  448.                (CAR (FLATTEN X))
  449.                (ZERO)))
  450.         (EQUAL (FLATTEN (CDR (GOPHER X)))
  451.            (IF (LISTP X)
  452.                (CDR (FLATTEN X))
  453.                (CONS (ZERO)
  454.                  (NIL))))
  455.         (EQUAL (QUOTIENT (TIMES Y X)
  456.                  Y)
  457.            (IF (ZEROP Y)
  458.                (ZERO)
  459.                (FIX X)))
  460.         (EQUAL (GET J (SET I VAL MEM))
  461.            (IF (EQP J I)
  462.                VAL
  463.                (GET J MEM)))))))
  464.  
  465. (DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST)
  466.        (COND ((TRUEP X TRUE-LST)
  467.           T)
  468.          ((FALSEP X FALSE-LST)
  469.           NIL)
  470.          ((ATOM X)
  471.           NIL)
  472.          ((EQ (CAR X)
  473.           (QUOTE IF))
  474.           (COND ((TRUEP (CADR X)
  475.                 TRUE-LST)
  476.              (TAUTOLOGYP (CADDR X)
  477.                  TRUE-LST FALSE-LST))
  478.             ((FALSEP (CADR X)
  479.                  FALSE-LST)
  480.              (TAUTOLOGYP (CAr (cDDDR X))
  481.                  TRUE-LST FALSE-LST))
  482.             (T (AND (TAUTOLOGYP (CADDR X)
  483.                     (CONS (CADR X)
  484.                           TRUE-LST)
  485.                     FALSE-LST)
  486.                 (TAUTOLOGYP (CAr (cDDDR X))
  487.                     TRUE-LST
  488.                     (CONS (CADR X)
  489.                           FALSE-LST))))))
  490.          (T NIL)))
  491.  
  492. (DEFUN TAUTP (X)
  493.        (TAUTOLOGYP (REWRITE X)
  494.            NIL NIL))
  495. (DEFUN TEST NIL
  496.        (PROG (ANS TERM)
  497.          (SETQ TERM
  498.            (APPLY-SUBST
  499.              (QUOTE ((X F (PLUS (PLUS A B)
  500.                     (PLUS C (ZERO))))
  501.                  (Y F (TIMES (TIMES A B)
  502.                      (PLUS C D)))
  503.                  (Z F (REVERSE (APPEND (APPEND A B)
  504.                            (NIL))))
  505.                  (U EQUAL (PLUS A B)
  506.                 (DIFFERENCE X Y))
  507.                  (W LESSP (REMAINDER A B)
  508.                 (MEMBER A (LENGTH B)))))
  509.              (QUOTE (IMPLIES (AND (IMPLIES X Y)
  510.                       (AND (IMPLIES Y Z)
  511.                            (AND (IMPLIES Z U)
  512.                             (IMPLIES U W))))
  513.                      (IMPLIES X W)))))
  514.          (SETQ ANS (TAUTP TERM))))
  515.  
  516. (DEFUN TRANS-OF-IMPLIES (N)
  517.        (LIST (QUOTE IMPLIES)
  518.          (TRANS-OF-IMPLIES1 N)
  519.          (LIST (QUOTE IMPLIES)
  520.            0 N)))
  521.  
  522. (DEFUN TRANS-OF-IMPLIES1 (N)
  523.        (COND ((EQUAL N 1)
  524.           (LIST (QUOTE IMPLIES)
  525.             0 1))
  526.          (T (LIST (QUOTE AND)
  527.               (LIST (QUOTE IMPLIES)
  528.                 (1- N)
  529.                 N)
  530.               (TRANS-OF-IMPLIES1 (1- N))))))
  531. (DEFUN TRUEP (X LST)
  532.        (OR (EQUAL X (QUOTE (T)))
  533.        (MEMBER X LST)))
  534.  
  535. (SETUP)
  536.  
  537. (define-timer boyer "Boyer" (test))
  538.  
  539. (qa-attempt "boyer" (test) nil)
  540.